theory zircon_DataStructure

imports Main 

begin

section "DEFINITION"

type_synonym SIZE_T = nat
type_synonym Memory_Addr = nat
type_synonym KOID = nat
type_synonym options = nat
type_synonym PRIO = int

definition LOWEST_PRIORITY where
        "LOWEST_PRIORITY ≡(0::int)"

definition DEFAULT_PRIORITY where
        "DEFAULT_PRIORITY ≡(16::int)"

definition HIGHEST_PRIORITY where
        "HIGHEST_PRIORITY ≡(31::int)"

(**)
definition UINT64_MAX where
        "UINT64_MAX ≡(999999::nat)"

definition DEFAULT_SIZE where
        "DEFAULT_SIZE ≡(8::nat)"

datatype RET = TEE_SUCCESS 
  | TEE_ERROR_ACCESS_DENIED | TEE_ERROR_GENERIC

datatype FLAGS = TEE_MEMORY_ACCESS_ANY_OWNER 
  | TEE_MEMORY_ACCESS_NONSECURE | TEE_MEMORY_ACCESS_SECURE | TEE_MEMORY_ACCESS_WRITE
  | TEE_MEMORY_ACCESS_READ

datatype ZX_STATUS_T = ZX_OK | ZX_ERR_INVALID_ARGS | ZX_ERR_WRONG_TYPE | ZX_ERR_ACCESS_DENIED | ZX_ERR_BAD_HANDLE | ZX_ERR_NOT_SUPPORTED | ZX_ERR_BAD_STATE

datatype ZX_RIGHTS_T = ZX_RIGHT_NONE | ZX_RIGHT_WRITE | ZX_DEFAULT_JOB_RIGHTS | ZX_DEFAULT_CHANNEL_RIGHTS 
                                     | ZX_DEFAULT_VMO_RIGHTS | ZX_RIGHT_SAME_RIGHTS | ZX_RIGHT_MAP | ZX_RIGHT_READ

datatype ZX_CACHE_POLICY = ZX_CACHE_POLICY_CACHED | ZX_CACHE_POLICY_UNCACHED | ZX_CACHE_POLICY_UNCACHED_DEVICE
                                                  | ZX_CACHE_POLICY_WRITE_COMBINING

datatype map_flags = ZX_VM_FLAG_SPECIFIC | ZX_VM_FLAG_SPECIFIC_OVERWRITE | ZX_VM_FLAG_PERM_READ | ZX_VM_FLAG_PERM_WRITE | 
                     ZX_VM_FLAG_PERM_EXECUTE | ZX_VM_FLAG_MAP_RANGE

(*Conditions handled by job policy.*)
datatype Conditions = ZX_POL_NEW_CHANNEL | ZX_POL_NEW_VMO 

datatype ZX_RSRC_KIND = ZX_RSRC_KIND_ROOT | ZX_RSRC_KIND_MMIO | ZX_RSRC_KIND_IOPORT | ZX_RSRC_KIND_IRQ 

datatype ZX_SIGNALS_T = ZX_SIGNAL_NONE | ZX_USER_SIGNAL_ALL

datatype futex_type = wait | wake

record Handle = 
        Kobject :: KOID
        rights :: ZX_RIGHTS_T
        process_bound :: KOID

section "Memory"

record Addr =
        first_addr ::Memory_Addr
        size :: SIZE_T

record Memory = Addr +
        ownership :: KOID
        access :: "KOID set"
        allocated :: bool

record resource = 
        memory :: Memory
        rsrc_kind :: ZX_RSRC_KIND

record vmo = 
        handle :: Handle
        memory :: "Memory option"
        rights :: ZX_RIGHTS_T
        cache_policy :: "ZX_CACHE_POLICY option"

section "PROCESS_AND_DISPATCHER"

record channel = 
        cid :: KOID
        handle0 :: Handle
        handle1 :: Handle

(*handle list*)
record thread =
        tid :: KOID
        handle :: Handle
        name :: string
        base_priority :: PRIO

record process =
        pid :: KOID
        handle :: Handle
        thread_set :: "thread set"
        addr :: "Addr list"

(*
A job is an object consisting of the following:
+ a reference to a parent job
+ a set of child jobs (each of whom has this job as parent)
+ a set of member [processes](process.md)
+ a set of policies [⚠ not implemented]
*)
record job = 
        jid :: KOID
        parent_handle :: Handle
        child_job :: "Handle list"
        pro_set :: "process set"
        rights :: ZX_RIGHTS_T


section "State"

record Dispatcher = 
        JobDispatcher :: "job list" 
        ThreadDispatcher :: "thread list"
        ProcessDispatcher :: "process list"
        VMODispatcher :: "vmo list"

record State = 
        current :: process
        object :: "KOID list"
        dispatcher :: Dispatcher
        handlelst :: "Handle list"
        channelst :: "channel list"
        nowAddr :: Memory_Addr
        memorylst :: "Memory list"
        futex :: futex_type
(*object*)
end